1  /-
  2  Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Author: Sébastien Gouëzel
  5  
  6  Construction of a good coupling between nonempty compact metric spaces, minimizing
  7  their Hausdorff distance. This construction is instrumental to study the Gromov-Hausdorff
  8  distance between nonempty compact metric spaces -/
  9  
 10  import topology.bounded_continuous_function topology.metric_space.gluing
src         └──────────────────────────────────┘ └──────────────────────────┘
 11  topology.metric_space.hausdorff_distance
src  └──────────────────────────────────────┘
 12  
 13  noncomputable theory
 14  open_locale classical
 15  open_locale topological_space
 16  universes u v w
 17  
 18  open classical lattice set function topological_space filter metric quotient
 19  open bounded_continuous_function
 20  open sum (inl inr)
 21  set_option class.instance_max_depth 50
doc             └──────────────────────┘
 22  
 23  local attribute [instance] metric_space_sum
 24  
 25  namespace Gromov_Hausdorff
 26  
 27  section Gromov_Hausdorff_realized
 28  /- This section shows that the Gromov-Hausdorff distance
 29  is realized. For this, we consider candidate distances on the disjoint union
 30  α ⊕ β of two compact nonempty metric spaces, almost realizing the Gromov-Hausdorff
 31  distance, and show that they form a compact family by applying Arzela-Ascoli
 32  theorem. The existence of a minimizer follows. -/
 33  
 34  section definitions
 35  variables (α : Type u) (β : Type v)
 36    [metric_space α] [compact_space α] [nonempty α]
id      └──────────┘     └───────────┘     └──────┘
src     └──────────┘     └───────────┘     └──────┘
typ     └──────────┘     └───────────┘     └──────┘
doc     └──────────┘     └───────────┘
 37    [metric_space β] [compact_space β] [nonempty β]
id      └──────────┘     └───────────┘     └──────┘
src     └──────────┘     └───────────┘     └──────┘
typ     └──────────┘     └───────────┘     └──────┘
doc     └──────────┘     └───────────┘
 38  
 39  @[reducible] private def prod_space_fun : Type* := ((α ⊕ β) × (α ⊕ β)) → ℝ
id                                                                     
src                                                                        
typ                                                                    
doc    └───────┘
 40  @[reducible] private def Cb : Type* := bounded_continuous_function ((α ⊕ β) × (α ⊕ β)) ℝ
id                                          └─────────────────────────┘              
src                                         └─────────────────────────┘                  
typ                                         └─────────────────────────┘              
doc    └───────┘                            └─────────────────────────┘
 41  
 42  private def max_var : nnreal :=
id                         └────┘
src                        └────┘
typ                        └────┘
doc                        └────┘
 43  2 * ⟨diam (univ : set α), diam_nonneg⟩ + 1 + 2 * ⟨diam (univ : set β), diam_nonneg⟩
id       └──┘  └──┘   └─┘    └─────────┘          └──┘  └──┘   └─┘    └─────────┘
src      └──┘  └──┘   └─┘     └─────────┘          └──┘  └──┘   └─┘     └─────────┘
typ      └──┘  └──┘   └─┘    └─────────┘          └──┘  └──┘   └─┘    └─────────┘
doc       └──┘                 └─────────┘             └──┘                 └─────────┘
 44  
 45  private lemma one_le_max_var : 1 ≤ max_var α β := calc
id                                     └─────┘  
src                                    └─────┘
typ                                    └─────┘  
 46    (1 : real) = 2 * 0 + 1 + 2 * 0 : by simp
id          └──┘
src         └──┘                           └────
typ         └──┘                           └────
doc                                        └────
txt                                        └────
par                                        └────
pid                                            
 47    ... ≤ 2 * diam (univ : set α) + 1 + 2 * diam (univ : set β) :
id               └──┘  └──┘   └─┘              └──┘  └──┘   └─┘
src  ─┘          └──┘  └──┘   └─┘              └──┘  └──┘   └─┘
typ  ─┘          └──┘  └──┘   └─┘              └──┘  └──┘   └─┘
doc  ─┘          └──┘                          └──┘
txt  ─┘
par  ─┘
pid  ─┘
 48    by apply_rules [add_le_add, mul_le_mul_of_nonneg_left, diam_nonneg, diam_nonneg]; norm_num
id                                                                           └───────┘
src       └───────────┘          └┘                         └┘           └┘  └───────┘  └────────
typ       └───────────┘          └┘                         └┘           └┘  └───────┘  └────────
doc       └───────────┘          └┘                         └┘           └┘  └───────┘  └────────
txt       └───────────┘          └┘                         └┘           └┘             └────────
par       └───────────┘          └┘                         └┘           └┘             └────────
pid                  └┘          └┘                         └┘           └┘                     
st                                                                           └────────────────────
 49  
src  
typ  
doc  
txt  
par  
pid  
st   
 50  /-- The set of functions on α ⊕ β that are candidates distances to realize the
 51  minimum of the Hausdorff distances between α and β in a coupling -/
 52  def candidates : set (prod_space_fun α β) :=
id                    └─┘  └────────────┘  
src                   └─┘  └────────────┘
typ                   └─┘  └────────────┘  
 53    {f | (((((∀x y : α, f (sum.inl x, sum.inl y) = dist x y)
id                       └─────┘   └─────┘    └──┘  
src                         └─────┘    └─────┘     └──┘
typ                      └─────┘   └─────┘    └──┘  
 54      ∧ (∀x y : β, f (sum.inr x, sum.inr y) = dist x y))
id                   └─────┘   └─────┘    └──┘  
src                    └─────┘    └─────┘     └──┘
typ                  └─────┘   └─────┘    └──┘  
 55      ∧ (∀x y,     f (x, y) = f (y, x)))
id                          
src                             
typ                         
 56      ∧ (∀x y z,   f (x, z) ≤ f (x, y) + f (y, z)))
id                               
src                                      
typ                              
 57      ∧ (∀x,       f (x, x) = 0))
id                       
src                          
typ                      
 58      ∧ (∀x y,     f (x, y) ≤ max_var α β) }
id                       └─────┘  
src                           └─────┘
typ                      └─────┘  
 59  
 60  /-- Version of the set of candidates in bounded_continuous_functions, to apply
 61  Arzela-Ascoli -/
 62  private def candidates_b : set (Cb α β) := {f : Cb α β | f.val ∈ candidates α β}
id                              └─┘  └┘           └┘     └──┘  └────────┘  
src                             └─┘  └┘             └┘        └──┘  └────────┘
typ                             └─┘  └┘           └┘     └──┘  └────────┘  
doc                                                                   └────────┘
 63  
 64  end definitions --section
 65  
 66  section constructions
 67  
 68  variables {α : Type u} {β : Type v}
 69  [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β]
id    └──────────┘     └───────────┘     └──────┘     └──────────┘     └───────────┘     └──────┘
src   └──────────┘     └───────────┘     └──────┘     └──────────┘     └───────────┘     └──────┘
typ   └──────────┘     └───────────┘     └──────┘     └──────────┘     └───────────┘     └──────┘
doc   └──────────┘     └───────────┘                  └──────────┘     └───────────┘
 70  {f : prod_space_fun α β} {x y z t : α ⊕ β}
id        └────────────┘                   
src       └────────────┘                   
typ       └────────────┘                   
 71  local attribute [instance, priority 10] inhabited_of_nonempty'
id                                           └────────────────────┘
src                                          └────────────────────┘
typ                                          └────────────────────┘
 72  
 73  private lemma max_var_bound : dist x y ≤ max_var α β := calc
id                                 └──┘    └─────┘  
src                                └──┘      └─────┘
typ                                └──┘    └─────┘  
 74    dist x y ≤ diam (univ : set (α ⊕ β)) :
id     └──┘       └──┘  └──┘   └─┘
src    └──┘       └──┘  └──┘   └─┘
typ    └──┘       └──┘  └──┘   └─┘
doc               └──┘
 75      dist_le_diam_of_mem (bounded_of_compact compact_univ) (mem_univ _) (mem_univ _)
id       └─────────────────┘  └────────────────┘ └──────────┘   └──────┘     └──────┘
src      └─────────────────┘  └────────────────┘ └──────────┘   └──────┘     └──────┘
typ      └─────────────────┘  └────────────────┘ └──────────┘   └──────┘     └──────┘
doc      └─────────────────┘  └────────────────┘
 76    ... = diam (inl '' (univ : set α) ∪ inr '' (univ : set β)) :
id           └──┘  └─┘     └──┘   └─┘      └─┘     └──┘   └─┘
src          └──┘  └─┘     └──┘   └─┘      └─┘     └──┘   └─┘
typ          └──┘  └─┘     └──┘   └─┘      └─┘     └──┘   └─┘
doc          └──┘
 77      by apply congr_arg; ext x y z; cases x; simp [mem_univ, mem_range_self]
id                                                     └──────┘  └────────────┘
src         └────┘           └───────┘  └────┘   └────┘└──────┘└┘└────────────┘└─
typ         └────┘           └───────┘  └────┘   └────┘└──────┘└┘└────────────┘└─
doc         └────┘           └───────┘  └────┘   └────┘        └┘              └─
txt         └────┘           └───────┘  └────┘   └────┘        └┘              └─
par         └────┘           └───────┘  └────┘   └────┘        └┘              └─
pid                            └────┘                      └┘              
st                                                     └─────────────────────────
 78    ... ≤ diam (inl '' (univ : set α)) + dist (inl (default α)) (inr (default β)) + diam (inr '' (univ : set β)) :
id           └──┘  └─┘ └┘  └──┘   └─┘     └──┘  └─┘  └─────┘     └─┘  └─────┘     └──┘  └─┘ └┘  └──┘   └─┘ 
src  ─┘      └──┘  └─┘ └┘  └──┘   └─┘      └──┘  └─┘  └─────┘      └─┘  └─────┘      └──┘  └─┘ └┘  └──┘   └─┘
typ  ─┘      └──┘  └─┘ └┘  └──┘   └─┘     └──┘  └─┘  └─────┘     └─┘  └─────┘     └──┘  └─┘ └┘  └──┘   └─┘ 
doc  ─┘      └──┘                                                                      └──┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
 79      diam_union (mem_image_of_mem _ (mem_univ _)) (mem_image_of_mem _ (mem_univ _))
id       └────────┘  └──────────────┘    └──────┘      └──────────────┘    └──────┘
src      └────────┘  └──────────────┘    └──────┘      └──────────────┘    └──────┘
typ      └────────┘  └──────────────┘    └──────┘      └──────────────┘    └──────┘
doc      └────────┘
 80    ... = diam (univ : set α) + (dist (default α) (default α) + 1 + dist (default β) (default β)) + diam (univ : set β) :
id           └──┘  └──┘   └─┘     └──┘  └─────┘    └─────┘       └──┘  └─────┘    └─────┘     └──┘  └──┘   └─┘ 
src          └──┘  └──┘   └─┘      └──┘  └─────┘     └─────┘        └──┘  └─────┘     └─────┘      └──┘  └──┘   └─┘
typ          └──┘  └──┘   └─┘     └──┘  └─────┘    └─────┘       └──┘  └─────┘    └─────┘     └──┘  └──┘   └─┘ 
doc          └──┘                                                                                      └──┘
 81      by { rw [isometry.diam_image isometry_on_inl, isometry.diam_image isometry_on_inr], refl }
id                └─────────────────┘ └─────────────┘  └─────────────────┘ └─────────────┘
src           └──┘└─────────────────┘└─────────────┘└┘└─────────────────┘└─────────────┘  └───┘
typ           └──┘└─────────────────┘└─────────────┘└┘└─────────────────┘└─────────────┘  └───┘
doc           └──┘└─────────────────┘└─────────────┘└┘└─────────────────┘└─────────────┘  └───┘
txt           └──┘                                  └┘                                    └───┘
par           └──┘                                  └┘                                    └───┘
pid             └┘                                  └┘                                        
st         └────────────────────────────────────────┘└───────────────────────────────────┘└──────┘└┘
 82    ... = 1 * diam (univ : set α) + 1 + 1 * diam (univ : set β) : by simp
id              └──┘  └──┘   └─┘          └──┘  └──┘   └─┘ 
src             └──┘  └──┘   └─┘           └──┘  └──┘   └─┘         └────
typ             └──┘  └──┘   └─┘          └──┘  └──┘   └─┘        └────
doc              └──┘                          └──┘                     └────
txt                                                                     └────
par                                                                     └────
pid                                                                         
st                                                                     └─────
 83    ... ≤ 2 * diam (univ : set α) + 1 + 2 * diam (univ : set β) :
id              └──┘  └──┘   └─┘          └──┘  └──┘   └─┘ 
src  ─┘         └──┘  └──┘   └─┘           └──┘  └──┘   └─┘
typ  ─┘         └──┘  └──┘   └─┘          └──┘  └──┘   └─┘ 
doc  ─┘          └──┘                          └──┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
 84    begin
st     └─────
 85      apply_rules [add_le_add, mul_le_mul_of_nonneg_right, diam_nonneg, diam_nonneg, le_refl],
id                    └────────┘  └────────────────────────┘  └─────────┘  └─────────┘  └─────┘
src      └───────────┘└────────┘└┘└────────────────────────┘└┘└─────────┘└┘└─────────┘└┘└─────┘
typ      └───────────┘└────────┘└┘└────────────────────────┘└┘└─────────┘└┘└─────────┘└┘└─────┘
doc      └───────────┘          └┘                          └┘└─────────┘└┘└─────────┘└┘       
txt      └───────────┘          └┘                          └┘           └┘           └┘       
par      └───────────┘          └┘                          └┘           └┘           └┘       
pid                 └┘          └┘                          └┘           └┘           └┘       
st   ──────────────────────────────────────────────────────────────────────────────────────────┘└─
 86      norm_num, norm_num
src      └──────┘  └────────
typ      └──────┘  └────────
doc      └──────┘  └────────
txt      └──────┘  └────────
par      └──────┘  └────────
pid                        
st   ───────────┘└──────────
 87    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
 88  
 89  private lemma candidates_symm (fA : f ∈ candidates α β) : f (x, y) = f (y ,x) := fA.1.1.1.2 x y
id                                         └────────┘                    └┘      
src                                         └────────┘                                 
typ                                        └────────┘                    └┘      
doc                                          └────────┘
 90  
 91  private lemma candidates_triangle (fA : f ∈ candidates α β) : f (x, z) ≤ f (x, y) + f (y, z) :=
id                                             └────────┘                     
src                                             └────────┘                            
typ                                            └────────┘                     
doc                                              └────────┘
 92    fA.1.1.2 x y z
id     └┘      
src        
typ    └┘      
 93  
 94  private lemma candidates_refl (fA : f ∈ candidates α β) : f (x, x) = 0 := fA.1.2 x
id                                         └────────┘                 └┘   
src                                         └────────┘                         
typ                                        └────────┘                 └┘   
doc                                          └────────┘
 95  
 96  private lemma candidates_nonneg (fA : f ∈ candidates α β) : 0 ≤ f (x, y) :=
id                                           └────────┘            
src                                           └────────┘             
typ                                          └────────┘            
doc                                            └────────┘
 97  begin
st   └─────
 98    have : 0 ≤ 2 * f (x, y) := calc
id                     
src    └───────┘└─┘  └┘ └───┘    
typ    └───────┘└─┘└┘└───┘    
doc    └───────┘ └─┘    └┘ └───┘    
txt    └───────┘ └─┘    └┘ └───┘    
par    └───────┘ └─┘    └┘ └───┘    
pid    └───┘└──┘ └─┘    └┘ └──┘    
st   ──────────────────────────────────
 99      0 = f (x, x) : (candidates_refl fA).symm
id                     └─────────────┘
src  ─────┘    └┘ └──┘ └─────────────┘  └──────
typ  ─────┘   └┘└──┘ └─────────────┘  └──────
doc  ─────┘    └┘ └──┘                  └──────
txt  ─────┘    └┘ └──┘                  └──────
par  ─────┘    └┘ └──┘                  └──────
pid  ─────┘    └┘ └──┘                  └──────
st   ─────────────────────────────────────────────
100      ... ≤ f (x, y) + f (y, x) : candidates_triangle fA
id                                  └─────────────────┘ └┘
src  ───────┘    └┘ └┘    └┘ └──┘└─────────────────┘  
typ  ───────┘    └┘ └┘   └┘ └──┘└─────────────────┘└┘
doc  ───────┘    └┘ └┘    └┘ └──┘                     
txt  ───────┘    └┘ └┘    └┘ └──┘                     
par  ───────┘    └┘ └┘    └┘ └──┘                     
pid  ───────┘    └┘ └┘    └┘ └──┘                     
st   ───────────────────────────────────────────────────────
101      ... = f (x, y) + f (x, y) : by rw [candidates_symm fA]
id                                         └─────────────┘ └┘
src  ───────┘    └┘ └┘   └┘ └──┘  └──┘└─────────────┘  └─
typ  ───────┘    └┘ └┘   └┘ └──┘  └──┘└─────────────┘└┘└─
doc  ───────┘    └┘ └┘    └┘ └──┘  └──┘                 └─
txt  ───────┘    └┘ └┘    └┘ └──┘  └──┘                 └─
par  ───────┘    └┘ └┘    └┘ └──┘  └──┘                 └─
pid  ───────┘    └┘ └┘    └┘ └──┘  └───┘                 └─
st   ─────────────────────────────────┘└─────────────────────┘
102      ... = 2 * f (x, y) : by ring,
src  ───┘└──┘ └─┘    └┘ └──┘  └──┘
typ  ───┘└──┘ └─┘    └┘ └──┘  └──┘
doc  ───┘└──┘ └─┘    └┘ └──┘  └──┘
txt  ───┘└──┘ └─┘    └┘ └──┘  └──┘
par  ───┘└──┘ └─┘    └┘ └──┘  └──┘
pid  ───────┘ └─┘    └┘ └──┘  └───┘
st   ───┘└─────────────────────┘└───┘
103    by linarith
src       └───────┘
typ       └───────┘
doc       └───────┘
txt       └───────┘
par       └───────┘
pid               
104  end
st   └─┘
105  
106  private lemma candidates_dist_inl (fA : f ∈ candidates α β) (x y: α) : f (inl x, inl y) = dist x y :=
id                                             └────────┘               └─┘   └─┘    └──┘  
src                                             └────────┘                   └─┘    └─┘     └──┘
typ                                            └────────┘               └─┘   └─┘    └──┘  
doc                                              └────────┘
107  fA.1.1.1.1.1 x y
id   └┘       
src        
typ  └┘       
108  
109  private lemma candidates_dist_inr (fA : f ∈ candidates α β) (x y : β) : f (inr x, inr y) = dist x y :=
id                                             └────────┘                └─┘   └─┘    └──┘  
src                                             └────────┘                    └─┘    └─┘     └──┘
typ                                            └────────┘                └─┘   └─┘    └──┘  
doc                                              └────────┘
110  fA.1.1.1.1.2 x y
id   └┘       
src        
typ  └┘       
111  
112  private lemma candidates_le_max_var (fA : f ∈ candidates α β) : f (x, y) ≤ max_var α β :=
id                                               └────────┘            └─────┘  
src                                               └────────┘                 └─────┘
typ                                              └────────┘            └─────┘  
doc                                                └────────┘
113  fA.2 x y
id   └┘   
src    
typ  └┘   
114  
115  /-- candidates are bounded by max_var α β -/
116  private lemma candidates_dist_bound  (fA : f ∈ candidates α β) :
id                                                └────────┘  
src                                                └────────┘
typ                                               └────────┘  
doc                                                 └────────┘
117    ∀ {x y : α ⊕ β}, f (x, y) ≤ max_var α β * dist x y
id                        └─────┘    └──┘  
src                             └─────┘      └──┘
typ                       └─────┘    └──┘  
118  | (inl x) (inl y) := calc
id             └─┘ 
src             └─┘
typ            └─┘ 
119      f (inl x, inl y) = dist x y : candidates_dist_inl fA x y
id        └─┘    └─┘      └──┘       └─────────────────┘ └┘
src        └─┘    └─┘      └──┘       └─────────────────┘
typ       └─┘    └─┘      └──┘       └─────────────────┘ └┘
120      ... = dist (inl x) (inl y) : by { rw @sum.dist_eq α β, refl }
id             └──┘  └─┘     └─┘               └─────────┘  
src            └──┘  └─┘     └─┘           └─┘ └─────────┘    └───┘
typ            └──┘  └─┘     └─┘           └─┘ └─────────┘  └───┘
doc                                        └─┘                └───┘
txt                                        └─┘                └───┘
par                                        └─┘                └───┘
pid                                                              
st                                      └────────────────────┘└─────┘└┘
121      ... = 1 * dist (inl x) (inl y) : by simp
id                └──┘  └─┘     └─┘
src               └──┘  └─┘     └─┘         └────
typ               └──┘  └─┘     └─┘         └────
doc                                          └────
txt                                          └────
par                                          └────
pid                                              
st                                          └─────
122      ... ≤ max_var α β * dist (inl x) (inl y) :
id             └─────┘    └──┘  └─┘     └─┘
src  ───┘      └─────┘      └──┘  └─┘     └─┘
typ  ───┘      └─────┘    └──┘  └─┘     └─┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘
123        mul_le_mul_of_nonneg_right (one_le_max_var α β) dist_nonneg
id         └────────────────────────┘  └────────────┘    └─────────┘
src        └────────────────────────┘  └────────────┘      └─────────┘
typ        └────────────────────────┘  └────────────┘    └─────────┘
124  | (inl x) (inr y) := calc
id      └─┘    └─┘ 
src     └─┘     └─┘
typ     └─┘    └─┘ 
125      f (inl x, inr y) ≤ max_var α β : candidates_le_max_var fA
id        └─┘    └─┘      └─────┘     └───────────────────┘ └┘
src        └─┘    └─┘      └─────┘       └───────────────────┘
typ       └─┘    └─┘      └─────┘     └───────────────────┘ └┘
126      ... = max_var α β * 1 : by simp
id             └─────┘   
src            └─────┘             └────
typ            └─────┘           └────
doc                                 └────
txt                                 └────
par                                 └────
pid                                     
st                                 └─────
127      ... ≤ max_var α β * dist (inl x) (inr y) :
id             └─────┘    └──┘  └─┘     └─┘
src  ───┘      └─────┘      └──┘  └─┘     └─┘
typ  ───┘      └─────┘    └──┘  └─┘     └─┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘
128        mul_le_mul_of_nonneg_left sum.one_dist_le (le_trans (zero_le_one) (one_le_max_var α β))
id         └───────────────────────┘ └─────────────┘  └──────┘  └─────────┘   └────────────┘  
src        └───────────────────────┘ └─────────────┘  └──────┘  └─────────┘   └────────────┘
typ        └───────────────────────┘ └─────────────┘  └──────┘  └─────────┘   └────────────┘  
129  | (inr x) (inl y) := calc
id      └─┘    └─┘ 
src     └─┘     └─┘
typ     └─┘    └─┘ 
130      f (inr x, inl y) ≤ max_var α β : candidates_le_max_var fA
id        └─┘    └─┘      └─────┘     └───────────────────┘ └┘
src        └─┘    └─┘      └─────┘       └───────────────────┘
typ       └─┘    └─┘      └─────┘     └───────────────────┘ └┘
131      ... = max_var α β * 1 : by simp
id             └─────┘   
src            └─────┘             └────
typ            └─────┘           └────
doc                                 └────
txt                                 └────
par                                 └────
pid                                     
st                                 └─────
132      ... ≤ max_var α β * dist (inl x) (inr y) :
id             └─────┘    └──┘  └─┘     └─┘
src  ───┘      └─────┘      └──┘  └─┘     └─┘
typ  ───┘      └─────┘    └──┘  └─┘     └─┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘
133        mul_le_mul_of_nonneg_left sum.one_dist_le (le_trans (zero_le_one) (one_le_max_var α β))
id         └───────────────────────┘ └─────────────┘  └──────┘  └─────────┘   └────────────┘  
src        └───────────────────────┘ └─────────────┘  └──────┘  └─────────┘   └────────────┘
typ        └───────────────────────┘ └─────────────┘  └──────┘  └─────────┘   └────────────┘  
134  | (inr x) (inr y) := calc
id             └─┘ 
src             └─┘
typ            └─┘ 
135      f (inr x, inr y) = dist x y : candidates_dist_inr fA x y
id        └─┘    └─┘      └──┘       └─────────────────┘ └┘
src        └─┘    └─┘      └──┘       └─────────────────┘
typ       └─┘    └─┘      └──┘       └─────────────────┘ └┘
136      ... = dist (inr x) (inr y) : by { rw @sum.dist_eq α β, refl }
id             └──┘  └─┘     └─┘               └─────────┘  
src            └──┘  └─┘     └─┘           └─┘ └─────────┘    └───┘
typ            └──┘  └─┘     └─┘           └─┘ └─────────┘  └───┘
doc                                        └─┘                └───┘
txt                                        └─┘                └───┘
par                                        └─┘                └───┘
pid                                                              
st                                      └────────────────────┘└─────┘└┘
137      ... = 1 * dist (inr x) (inr y) : by simp
id                └──┘  └─┘     └─┘
src               └──┘  └─┘     └─┘         └────
typ               └──┘  └─┘     └─┘         └────
doc                                          └────
txt                                          └────
par                                          └────
pid                                              
st                                          └─────
138      ... ≤ max_var α β * dist (inr x) (inr y) :
id             └─────┘    └──┘  └─┘     └─┘
src  ───┘      └─────┘      └──┘  └─┘     └─┘
typ  ───┘      └─────┘    └──┘  └─┘     └─┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘
139        mul_le_mul_of_nonneg_right (one_le_max_var α β) dist_nonneg
id         └────────────────────────┘  └────────────┘    └─────────┘
src        └────────────────────────┘  └────────────┘      └─────────┘
typ        └────────────────────────┘  └────────────┘    └─────────┘
140  
141  /-- Technical lemma to prove that candidates are Lipschitz -/
142  private lemma candidates_lipschitz_aux (fA : f ∈ candidates α β) : f (x, y) - f (z, t) ≤ 2 * max_var α β * dist (x, y) (z, t) :=
id                                                  └────────┘                     └─────┘    └──┘       
src                                                  └────────┘                             └─────┘      └──┘       
typ                                                 └────────┘                     └─────┘    └──┘       
doc                                                   └────────┘
143  calc
144    f (x, y) - f(z, t) ≤ f (x, t) + f (t, y) - f (z, t) : add_le_add_right (candidates_triangle fA) _
id                                    └──────────────┘  └─────────────────┘ └┘
src                                                  └──────────────┘  └─────────────────┘
typ                                   └──────────────┘  └─────────────────┘ └┘
145    ... ≤ (f (x, z) + f (z, t) + f(t, y)) - f (z, t) :
id                                 
src                                        
typ                                
146      add_le_add_right (add_le_add_right (candidates_triangle fA) _ ) _
id       └──────────────┘  └──────────────┘  └─────────────────┘ └┘
src      └──────────────┘  └──────────────┘  └─────────────────┘
typ      └──────────────┘  └──────────────┘  └─────────────────┘ └┘
147    ... = f (x, z) + f (t, y) : by simp
id                    
src                                └────
typ                          └────
doc                                   └────
txt                                   └────
par                                   └────
pid                                       
st                                   └─────
148    ... ≤ max_var α β * dist x z + max_var α β * dist t y :
id           └─────┘    └──┘    └─────┘    └──┘  
src  ─┘      └─────┘      └──┘      └─────┘      └──┘
typ  ─┘      └─────┘    └──┘    └─────┘    └──┘  
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
149      add_le_add (candidates_dist_bound fA) (candidates_dist_bound fA)
id       └────────┘  └───────────────────┘ └┘   └───────────────────┘ └┘
src      └────────┘  └───────────────────┘      └───────────────────┘
typ      └────────┘  └───────────────────┘ └┘   └───────────────────┘ └┘
doc                  └───────────────────┘      └───────────────────┘
150    ... ≤ max_var α β * max (dist x z) (dist t y) + max_var α β * max (dist x z) (dist t y) :
id           └─────┘    └─┘  └──┘     └──┘     └─────┘    └─┘  └──┘     └──┘  
src          └─────┘      └─┘  └──┘       └──┘       └─────┘      └─┘  └──┘       └──┘
typ          └─────┘    └─┘  └──┘     └──┘     └─────┘    └─┘  └──┘     └──┘  
151    begin
st     └─────
152      apply add_le_add,
id             └────────┘
src      └────┘└────────┘
typ      └────┘└────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────────────┘└─
153      apply mul_le_mul_of_nonneg_left (le_max_left (dist x z) (dist t y)) (le_trans zero_le_one (one_le_max_var α β)),
id             └───────────────────────┘  └─────────┘           └──┘      └──────┘ └─────────┘  └────────────┘  
src      └────┘└───────────────────────┘ └─────────┘       └┘ └──┘  └─┘ └──────┘└─────────┘ └────────────┘  └┘
typ      └────┘└───────────────────────┘ └─────────┘     └┘ └──┘└─┘ └──────┘└─────────┘ └────────────┘└┘
doc      └────┘                                            └┘       └─┘                                     └┘
txt      └────┘                                            └┘       └─┘                                     └┘
par      └────┘                                            └┘       └─┘                                     └┘
pid                                                       └┘       └─┘                                     └┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
154      apply mul_le_mul_of_nonneg_left (le_max_right (dist x z) (dist t y)) (le_trans zero_le_one (one_le_max_var α β)),
id             └───────────────────────┘  └──────────┘           └──┘      └──────┘ └─────────┘  └────────────┘  
src      └────┘└───────────────────────┘ └──────────┘       └┘ └──┘  └─┘ └──────┘└─────────┘ └────────────┘  └┘
typ      └────┘└───────────────────────┘ └──────────┘     └┘ └──┘└─┘ └──────┘└─────────┘ └────────────┘└┘
doc      └────┘                                             └┘       └─┘                                     └┘
txt      └────┘                                             └┘       └─┘                                     └┘
par      └────┘                                             └┘       └─┘                                     └┘
pid                                                        └┘       └─┘                                     └┘
st   ───────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
155    end
st   ────┘
156    ... = 2 * max_var α β * max (dist x z) (dist y t) :
id              └─────┘    └─┘  └──┘     └──┘  
src             └─────┘      └─┘  └──┘       └──┘
typ             └─────┘    └─┘  └──┘     └──┘  
157      by { simp [dist_comm], ring }
id                  └───────┘
src           └────┘└───────┘  └───┘
typ           └────┘└───────┘  └───┘
doc           └────┘           └───┘
txt           └────┘           └───┘
par           └────┘           └───┘
pid                              
st         └─────────────────┘└─────┘└┘
158    ... = 2 * max_var α β * dist (x, y) (z, t) : by refl
id              └─────┘    └──┘       
src             └─────┘      └──┘                  └────
typ             └─────┘    └──┘              └────
doc                                                    └────
txt                                                    └────
par                                                    └────
pid                                                        
st                                                    └─────
159  
src  
typ  
doc  
txt  
par  
pid  
st   
160  /-- Candidates are Lipschitz -/
161  private lemma candidates_lipschitz (fA : f ∈ candidates α β) :
id                                              └────────┘  
src                                              └────────┘
typ                                             └────────┘  
doc                                               └────────┘
162    lipschitz_with (2 * max_var α β) f :=
id     └────────────┘     └─────┘    
src    └────────────┘     └─────┘
typ    └────────────┘     └─────┘    
doc    └────────────┘
163  begin
st   └─────
164    rintros ⟨x, y⟩ ⟨z, t⟩,
src    └───────────────────┘
typ    └───────────────────┘
doc    └───────────────────┘
txt    └───────────────────┘
par    └───────────────────┘
pid           └────────────┘
st   ──────────────────────┘└─
165    rw real.dist_eq,
id        └──────────┘
src    └─┘└──────────┘
typ    └─┘└──────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────────────┘└─
166    apply abs_le_of_le_of_neg_le,
id           └────────────────────┘
src    └────┘└────────────────────┘
typ    └────┘└────────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────────────────────────┘└─
167    { exact candidates_lipschitz_aux fA },
id             └──────────────────────┘ └┘
src      └────┘└──────────────────────┘  
typ      └────┘└──────────────────────┘└┘
doc      └────┘└──────────────────────┘  
txt      └────┘                          
par      └────┘                          
pid                                     
st   ───┘└────────────────────────────────┘└┘
168    { have : -(f (x, y) - f (z, t)) = f (z, t) - f (x, y), by ring,
id                                                
src      └─────┘    └┘ └┘   └┘ └─┘   └┘ └┘   └┘      └──┘
typ      └─────┘    └┘ └┘   └┘ └─┘  └┘└┘ └┘     └──┘
doc      └─────┘     └┘ └┘    └┘ └─┘    └┘ └┘    └┘      └──┘
txt      └─────┘     └┘ └┘    └┘ └─┘    └┘ └┘    └┘      └──┘
par      └─────┘     └┘ └┘    └┘ └─┘    └┘ └┘    └┘      └──┘
pid      └───┘└┘     └┘ └┘    └┘ └─┘    └┘ └┘    └┘ 
st   ──────────────────────────────────────────────────────┘         └─
169      rw [this, dist_comm],
id           └──┘  └───────┘
src      └──┘    └┘└───────┘
typ      └──┘└──┘└┘└───────┘
doc      └──┘    └┘         
txt      └──┘    └┘         
par      └──┘    └┘         
pid        └┘    └┘         
st   ───────────┘└─────────┘└──
170      exact candidates_lipschitz_aux fA }
id             └──────────────────────┘ └┘
src      └────┘└──────────────────────┘  
typ      └────┘└──────────────────────┘└┘
doc      └────┘└──────────────────────┘  
txt      └────┘                          
par      └────┘                          
pid                                     
st   ─────────────────────────────────────┘└─
171  end
st   ──┘
172  
173  /-- candidates give rise to elements of bounded_continuous_functions -/
174  def candidates_b_of_candidates (f : prod_space_fun α β) (fA : f ∈ candidates α β) : Cb α β :=
id                                       └────────────┘            └────────┘      └┘  
src                                      └────────────┘               └────────┘        └┘
typ                                      └────────────┘            └────────┘      └┘  
doc                                                                    └────────┘
175  bounded_continuous_function.mk_of_compact f (candidates_lipschitz fA).to_continuous
id   └───────────────────────────────────────┘   └──────────────────┘ └┘ └───────────┘
src  └───────────────────────────────────────┘    └──────────────────┘    └───────────┘
typ  └───────────────────────────────────────┘   └──────────────────┘ └┘ └───────────┘
doc  └───────────────────────────────────────┘    └──────────────────┘    └───────────┘
176  
177  lemma candidates_b_of_candidates_mem (f : prod_space_fun α β) (fA : f ∈ candidates α β) :
id                                             └────────────┘            └────────┘  
src                                            └────────────┘               └────────┘
typ                                            └────────────┘            └────────┘  
doc                                                                          └────────┘
178    candidates_b_of_candidates f fA ∈ candidates_b α β := fA
id     └────────────────────────┘  └┘  └──────────┘      └┘
src    └────────────────────────┘       └──────────┘
typ    └────────────────────────┘  └┘  └──────────┘      └┘
doc    └────────────────────────┘        └──────────┘
179  
180  /-- The distance on α ⊕ β is a candidate -/
181  private lemma dist_mem_candidates : (λp : (α ⊕ β) × (α ⊕ β), dist p.1 p.2) ∈ candidates α β :=
id                                                         └──┘       └────────┘  
src                                                            └──┘         └────────┘
typ                                                        └──┘       └────────┘  
doc                                                                               └────────┘
182  begin
st   └─────
183    simp only [candidates, dist_comm, forall_const, and_true, add_comm, eq_self_iff_true,
id                └────────┘  └───────┘  └──────────┘  └──────┘  └──────┘  └──────────────┘
src    └─────────┘└────────┘└┘└───────┘└┘└──────────┘└┘└──────┘└┘└──────┘└┘└──────────────┘└─
typ    └─────────┘└────────┘└┘└───────┘└┘└──────────┘└┘└──────┘└┘└──────┘└┘└──────────────┘└─
doc    └─────────┘└────────┘└┘         └┘            └┘        └┘        └┘                └─
txt    └─────────┘          └┘         └┘            └┘        └┘        └┘                └─
par    └─────────┘          └┘         └┘            └┘        └┘        └┘                └─
pid        └──┘└┘          └┘         └┘            └┘        └┘        └┘                └─
st   ────────────────────────────────────────────────────────────────────────────────────────
184               and_self, sum.forall, set.mem_set_of_eq, dist_self],
id                └──────┘  └────────┘  └───────────────┘  └───────┘
src  ────────────┘└──────┘└┘└────────┘└┘└───────────────┘└┘└───────┘
typ  ────────────┘└──────┘└┘└────────┘└┘└───────────────┘└┘└───────┘
doc  ────────────┘        └┘          └┘                 └┘         
txt  ────────────┘        └┘          └┘                 └┘         
par  ────────────┘        └┘          └┘                 └┘         
pid  ────────────┘        └┘          └┘                 └┘         
st   ───────────────────────────────────────────────────────────────┘└─
185    repeat { split
src    └───────┘└─────
typ    └───────┘└─────
doc    └───────┘└─────
txt    └───────┘└─────
par    └───────┘└─────
pid          └────────
st   ─────────────────
186      <|> exact (λa y z, dist_triangle_left _ _ _)
id                          └────────────────┘
src  ───┘└──┘└────┘  └─────┘└────────────────┘└───────
typ  ───┘└──┘└────┘  └─────┘└────────────────┘└───────
doc  ───┘└──┘└────┘  └─────┘                  └───────
txt  ───┘└──┘└────┘  └─────┘                  └───────
par  ───┘└──┘└────┘  └─────┘                  └───────
pid  ─────────────┘  └─────┘                  └───────
st   ─────────────────────────────────────────────────
187      <|> exact (λx y, by refl)
src  ───┘└──┘└────┘  └───┘  └──┘└─
typ  ───┘└──┘└────┘  └───┘  └──┘└─
doc  ───┘└──┘└────┘  └───┘  └──┘└─
txt  ───┘└──┘└────┘  └───┘  └──┘└─
par  ───┘└──┘└────┘  └───┘  └──┘└─
pid  ─────────────┘  └───┘  └──────
st   ──────────────────────┘└───┘└─
188      <|> exact (λx y, max_var_bound) }
id                        └───────────┘
src  ───┘└──┘└────┘  └───┘└───────────┘└┘└┘
typ  ───┘└──┘└────┘  └───┘└───────────┘└┘└┘
doc  ───┘└──┘└────┘  └───┘             └┘└┘
txt  ───┘└──┘└────┘  └───┘             └┘└┘
par  ───┘└──┘└────┘  └───┘             └┘└┘
pid  ─────────────┘  └───┘             └─┘
st   ───────────────────────────────────┘
189  end
st   └─┘
190  
191  def candidates_b_dist (α : Type u) (β : Type v) [metric_space α] [compact_space α] [inhabited α]
id                                                    └──────────┘    └───────────┘    └───────┘ 
src                                                   └──────────┘     └───────────┘     └───────┘
typ                                                   └──────────┘    └───────────┘    └───────┘ 
doc                                                   └──────────┘     └───────────┘
192    [metric_space β] [compact_space β] [inhabited β] : Cb α β := candidates_b_of_candidates _ dist_mem_candidates
id      └──────────┘    └───────────┘    └───────┘     └┘      └────────────────────────┘   └─────────────────┘
src     └──────────┘     └───────────┘     └───────┘      └┘        └────────────────────────┘   └─────────────────┘
typ     └──────────┘    └───────────┘    └───────┘     └┘      └────────────────────────┘   └─────────────────┘
doc     └──────────┘     └───────────┘                              └────────────────────────┘   └─────────────────┘
193  
194  lemma candidates_b_dist_mem_candidates_b : candidates_b_dist α β ∈ candidates_b α β :=
id                                              └───────────────┘    └──────────┘  
src                                             └───────────────┘      └──────────┘
typ                                             └───────────────┘    └──────────┘  
doc                                                                     └──────────┘
195  candidates_b_of_candidates_mem _ _
id   └────────────────────────────┘
src  └────────────────────────────┘
typ  └────────────────────────────┘
196  
197  private lemma candidates_b_nonempty : (candidates_b α β).nonempty :=
id                                          └──────────┘   └──────┘
src                                         └──────────┘     └──────┘
typ                                         └──────────┘   └──────┘
doc                                         └──────────┘     └──────┘
198  ⟨_,  candidates_b_dist_mem_candidates_b⟩
id        └────────────────────────────────┘
src       └────────────────────────────────┘
typ       └────────────────────────────────┘
199  
200  /-- To apply Arzela-Ascoli, we need to check that the set of candidates is closed and equicontinuous.
201  Equicontinuity follows from the Lipschitz control, we check closedness -/
202  private lemma closed_candidates_b : is_closed (candidates_b α β) :=
id                                       └───────┘  └──────────┘  
src                                      └───────┘  └──────────┘
typ                                      └───────┘  └──────────┘  
doc                                      └───────┘  └──────────┘
203  begin
st   └─────
204    have I1 : ∀x y, is_closed {f : Cb α β | f (inl x, inl y) = dist x y} :=
id                     └───────┘     └┘              └─┘     └──┘
src    └────────┘ └─┘ └───────┘└──┘└┘  └─┘     └┘└─┘ └┘└──┘  └────
typ    └────────┘ └─┘ └───────┘└──┘└┘└─┘     └┘└─┘ └┘└──┘  └────
doc    └────────┘ └─┘ └───────┘ └──┘    └─┘      └┘    └┘       └────
txt    └────────┘ └─┘           └──┘    └─┘      └┘    └┘       └────
par    └────────┘ └─┘           └──┘    └─┘      └┘    └┘       └────
pid    └─────┘└─┘ └─┘           └──┘    └─┘      └┘    └┘       └───
st   ──────────────────────────────────────────────────────────────────────────
205      λx y, is_closed_eq continuous_evalx continuous_const,
id             └──────────┘ └──────────────┘ └──────────────┘
src  ───┘ └───┘└──────────┘└──────────────┘└──────────────┘
typ  ───┘ └───┘└──────────┘└──────────────┘└──────────────┘
doc  ───┘ └───┘            └──────────────┘
txt  ───┘ └───┘                            
par  ───┘ └───┘                            
pid  ───┘ └───┘                            
st   ───────────────────────────────────────────────────────┘└─
206    have I2 : ∀x y, is_closed {f : Cb α β | f (inr x, inr y) = dist x y } :=
id                     └───────┘     └┘              └─┘      └──┘
src    └────────┘ └─┘ └───────┘└──┘└┘  └─┘     └┘└─┘ └┘ └──┘  └─────
typ    └────────┘ └─┘ └───────┘└──┘└┘└─┘     └┘└─┘ └┘ └──┘  └─────
doc    └────────┘ └─┘ └───────┘ └──┘    └─┘      └┘    └┘       └─────
txt    └────────┘ └─┘           └──┘    └─┘      └┘    └┘       └─────
par    └────────┘ └─┘           └──┘    └─┘      └┘    └┘       └─────
pid    └─────┘└─┘ └─┘           └──┘    └─┘      └┘    └┘       └┘└───
st   ───────────────────────────────────────────────────────────────────────────
207      λx y, is_closed_eq continuous_evalx continuous_const,
id             └──────────┘ └──────────────┘ └──────────────┘
src  ───┘ └───┘└──────────┘└──────────────┘└──────────────┘
typ  ───┘ └───┘└──────────┘└──────────────┘└──────────────┘
doc  ───┘ └───┘            └──────────────┘
txt  ───┘ └───┘                            
par  ───┘ └───┘                            
pid  ───┘ └───┘                            
st   ───────────────────────────────────────────────────────┘└─
208    have I3 : ∀x y, is_closed {f : Cb α β | f (x, y) = f (y, x)} :=
id                     └───────┘     └┘                  
src    └────────┘ └─┘ └───────┘└──┘└┘  └─┘   └┘ └┘   └┘ └─────
typ    └────────┘ └─┘ └───────┘└──┘└┘└─┘   └┘ └┘   └┘ └─────
doc    └────────┘ └─┘ └───────┘ └──┘    └─┘   └┘ └┘    └┘ └─────
txt    └────────┘ └─┘           └──┘    └─┘   └┘ └┘    └┘ └─────
par    └────────┘ └─┘           └──┘    └─┘   └┘ └┘    └┘ └─────
pid    └─────┘└─┘ └─┘           └──┘    └─┘   └┘ └┘    └┘ └┘└───
st   ──────────────────────────────────────────────────────────────────
209      λx y, is_closed_eq continuous_evalx continuous_evalx,
id             └──────────┘                  └──────────────┘
src  ───┘ └───┘└──────────┘                └──────────────┘
typ  ───┘ └───┘└──────────┘                └──────────────┘
doc  ───┘ └───┘                            └──────────────┘
txt  ───┘ └───┘                            
par  ───┘ └───┘                            
pid  ───┘ └───┘                            
st   ───────────────────────────────────────────────────────┘└─
210    have I4 : ∀x y z, is_closed {f : Cb α β | f (x, z) ≤ f (x, y) + f (y, z)} :=
id                       └───────┘     └┘                           
src    └────────┘ └───┘ └───────┘└──┘└┘  └─┘   └┘ └┘   └┘ └┘  └┘ └─────
typ    └────────┘ └───┘ └───────┘└──┘└┘└─┘   └┘ └┘   └┘ └┘  └┘ └─────
doc    └────────┘ └───┘ └───────┘ └──┘    └─┘   └┘ └┘    └┘ └┘    └┘ └─────
txt    └────────┘ └───┘           └──┘    └─┘   └┘ └┘    └┘ └┘    └┘ └─────
par    └────────┘ └───┘           └──┘    └─┘   └┘ └┘    └┘ └┘    └┘ └─────
pid    └─────┘└─┘ └───┘           └──┘    └─┘   └┘ └┘    └┘ └┘    └┘ └┘└───
st   ───────────────────────────────────────────────────────────────────────────────
211      λx y z, is_closed_le continuous_evalx (continuous_evalx.add continuous_evalx),
id               └──────────┘                   └──────────────────┘ └──────────────┘
src  ───┘ └─────┘└──────────┘                 └──────────────────┘└──────────────┘
typ  ───┘ └─────┘└──────────┘                 └──────────────────┘└──────────────┘
doc  ───┘ └─────┘                                                 └──────────────┘
txt  ───┘ └─────┘                                                                 
par  ───┘ └─────┘                                                                 
pid  ───┘ └─────┘                                                                 
st   ────────────────────────────────────────────────────────────────────────────────┘└─
212    have I5 : ∀x, is_closed {f : Cb α β | f (x, x) = 0} :=
id                   └───────┘     └┘       
src    └────────┘  └───────┘└──┘└┘  └─┘  └┘ └┘ └──────
typ    └────────┘  └───────┘└──┘└┘└─┘  └┘ └┘ └──────
doc    └────────┘  └───────┘ └──┘    └─┘   └┘ └┘ └──────
txt    └────────┘            └──┘    └─┘   └┘ └┘ └──────
par    └────────┘            └──┘    └─┘   └┘ └┘ └──────
pid    └─────┘└─┘            └──┘    └─┘   └┘ └┘ └─┘└───
st   ─────────────────────────────────────────────────────────
213      λx, is_closed_eq continuous_evalx continuous_const,
id           └──────────┘ └──────────────┘ └──────────────┘
src  ───┘ └─┘└──────────┘└──────────────┘└──────────────┘
typ  ───┘ └─┘└──────────┘└──────────────┘└──────────────┘
doc  ───┘ └─┘            └──────────────┘
txt  ───┘ └─┘                            
par  ───┘ └─┘                            
pid  ───┘ └─┘                            
st   ─────────────────────────────────────────────────────┘└─
214    have I6 : ∀x y, is_closed {f : Cb α β | f (x, y) ≤ max_var α β} :=
id                     └───────┘     └┘                 └─────┘  
src    └────────┘ └─┘ └───────┘└──┘└┘  └─┘  └┘ └┘ └─────┘  └────
typ    └────────┘ └─┘ └───────┘└──┘└┘  └─┘  └┘ └┘ └─────┘└────
doc    └────────┘ └─┘ └───────┘ └──┘    └─┘   └┘ └┘          └────
txt    └────────┘ └─┘           └──┘    └─┘   └┘ └┘          └────
par    └────────┘ └─┘           └──┘    └─┘   └┘ └┘          └────
pid    └─────┘└─┘ └─┘           └──┘    └─┘   └┘ └┘          └───
st   ─────────────────────────────────────────────────────────────────────
215      λx y, is_closed_le continuous_evalx continuous_const,
id             └──────────┘ └──────────────┘ └──────────────┘
src  ───┘ └───┘└──────────┘└──────────────┘└──────────────┘
typ  ───┘ └───┘└──────────┘└──────────────┘└──────────────┘
doc  ───┘ └───┘            └──────────────┘
txt  ───┘ └───┘                            
par  ───┘ └───┘                            
pid  ───┘ └───┘                            
st   ───────────────────────────────────────────────────────┘└─
216    have : candidates_b α β = (⋂x y, {f : Cb α β | f ((@inl α β x), (@inl α β y)) = dist x y})
id            └──────────┘                                               └─┘
src    └─────┘└──────────┘     └─┘  └──┘    └─┘          └─┘  └─┘   └─┘       └──
typ    └─────┘└──────────┘     └─┘  └──┘    └─┘          └─┘  └─┘   └─┘       └──
doc    └─────┘└──────────┘     └─┘  └──┘    └─┘          └─┘        └─┘       └──
txt    └─────┘                 └─┘  └──┘    └─┘          └─┘        └─┘       └──
par    └─────┘                 └─┘  └──┘    └─┘          └─┘        └─┘       └──
pid    └───┘└┘                 └─┘  └──┘    └─┘          └─┘        └─┘       └──
st   ─────────────────────────────────────────────────────────────────────────────────────────────
217                 ∩ (⋂x y, {f : Cb α β | f ((@inr α β x), (@inr α β y)) = dist x y})
id                                                           └─┘           └──┘
src  ──────────────┘  └─┘  └──┘    └─┘          └─┘  └─┘   └─┘ └──┘  └──
typ  ──────────────┘  └─┘  └──┘    └─┘          └─┘  └─┘   └─┘ └──┘  └──
doc  ──────────────┘   └─┘  └──┘    └─┘          └─┘        └─┘       └──
txt  ──────────────┘   └─┘  └──┘    └─┘          └─┘        └─┘       └──
par  ──────────────┘   └─┘  └──┘    └─┘          └─┘        └─┘       └──
pid  ──────────────┘   └─┘  └──┘    └─┘          └─┘        └─┘       └──
st   ──────────────────────────────────────────────────────────────────────────────────
218                 ∩ (⋂x y, {f : Cb α β | f (x, y) = f (y, x)})
src  ──────────────┘   └─┘  └──┘    └─┘   └┘ └┘    └┘ └───
typ  ──────────────┘   └─┘  └──┘    └─┘   └┘ └┘    └┘ └───
doc  ──────────────┘   └─┘  └──┘    └─┘   └┘ └┘    └┘ └───
txt  ──────────────┘   └─┘  └──┘    └─┘   └┘ └┘    └┘ └───
par  ──────────────┘   └─┘  └──┘    └─┘   └┘ └┘    └┘ └───
pid  ──────────────┘   └─┘  └──┘    └─┘   └┘ └┘    └┘ └───
st   ────────────────────────────────────────────────────────────
219                 ∩ (⋂x y z, {f : Cb α β | f (x, z) ≤ f (x, y) + f (y, z)})
src  ──────────────┘   └───┘  └──┘    └─┘   └┘ └┘    └┘ └┘    └┘ └───
typ  ──────────────┘   └───┘  └──┘    └─┘   └┘ └┘    └┘ └┘    └┘ └───
doc  ──────────────┘   └───┘  └──┘    └─┘   └┘ └┘    └┘ └┘    └┘ └───
txt  ──────────────┘   └───┘  └──┘    └─┘   └┘ └┘    └┘ └┘    └┘ └───
par  ──────────────┘   └───┘  └──┘    └─┘   └┘ └┘    └┘ └┘    └┘ └───
pid  ──────────────┘   └───┘  └──┘    └─┘   └┘ └┘    └┘ └┘    └┘ └───
st   ─────────────────────────────────────────────────────────────────────────
220                 ∩ (⋂x, {f : Cb α β | f (x, x) = 0})
id                      
src  ──────────────┘   └──┘    └─┘   └┘ └┘ └────
typ  ──────────────┘   └──┘    └─┘   └┘ └┘ └────
doc  ──────────────┘   └──┘    └─┘   └┘ └┘ └────
txt  ──────────────┘     └──┘    └─┘   └┘ └┘ └────
par  ──────────────┘     └──┘    └─┘   └┘ └┘ └────
pid  ──────────────┘     └──┘    └─┘   └┘ └┘ └────
st   ───────────────────────────────────────────────────
221                 ∩ (⋂x y, {f : Cb α β | f (x, y) ≤ max_var α β}) :=
id                               └┘                 └─────┘  
src  ──────────────┘   └─┘ └──┘└┘  └─┘  └┘ └┘ └─────┘  └─────
typ  ──────────────┘   └─┘ └──┘└┘  └─┘  └┘ └┘ └─────┘└─────
doc  ──────────────┘   └─┘  └──┘    └─┘   └┘ └┘          └─────
txt  ──────────────┘   └─┘  └──┘    └─┘   └┘ └┘          └─────
par  ──────────────┘   └─┘  └──┘    └─┘   └┘ └┘          └─────
pid  ──────────────┘   └─┘  └──┘    └─┘   └┘ └┘          └┘└───
st   ──────────────────────────────────────────────────────────────────
222      begin ext, unfold candidates_b, unfold candidates, simp [-sum.forall], refl end,
src  ───┘     └─┘└┘└─────────────────┘└┘└───────────────┘└┘└────────────────┘└┘└───┘└─┘
typ  ───┘     └─┘└┘└─────────────────┘└┘└───────────────┘└┘└────────────────┘└┘└───┘└─┘
doc  ───┘     └─┘└┘└─────────────────┘└┘└───────────────┘└┘└────────────────┘└┘└───┘└─┘
txt  ───┘     └─┘└┘└─────────────────┘└┘└───────────────┘└┘└────────────────┘└┘└───┘└─┘
par  ───┘     └─┘└┘└─────────────────┘└┘└───────────────┘└┘└────────────────┘└┘└───┘└─┘
pid  ───┘     └────────────────────────────────────────────────────────────────────────┘
st   ───┘└───────┘└───────────────────┘└─────────────────┘└──────────────────┘└─────┘└─┘└─
223    rw this,
id        └──┘
src    └─┘
typ    └─┘└──┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────┘└─
224    repeat { apply is_closed_inter _ _
id                    └─────────────┘
src    └───────┘└────┘└─────────────┘└────
typ    └───────┘└────┘└─────────────┘└────
doc    └───────┘└────┘               └────
txt    └───────┘└────┘               └────
par    └───────┘└────┘               └────
pid          └───────┘               └────
st   ─────────────────────────────────────
225         <|> apply is_closed_Inter _
id                    └─────────────┘
src  ──────┘└──┘└────┘└─────────────┘└──
typ  ──────┘└──┘└────┘└─────────────┘└──
doc  ──────┘└──┘└────┘               └──
txt  ──────┘└──┘└────┘               └──
par  ──────┘└──┘└────┘               └──
pid  ────────────────┘               └──
st   ───────────────────────────────────
226         <|> apply I1 _ _
id                    └┘
src  ──────┘└──┘└────┘  └────
typ  ──────┘└──┘└────┘└┘└────
doc  ──────┘└──┘└────┘  └────
txt  ──────┘└──┘└────┘  └────
par  ──────┘└──┘└────┘  └────
pid  ────────────────┘  └────
st   ────────────────────────
227         <|> apply I2 _ _
id                    └┘
src  ──────┘└──┘└────┘  └────
typ  ──────┘└──┘└────┘└┘└────
doc  ──────┘└──┘└────┘  └────
txt  ──────┘└──┘└────┘  └────
par  ──────┘└──┘└────┘  └────
pid  ────────────────┘  └────
st   ────────────────────────
228         <|> apply I3 _ _
id                    └┘
src  ──────┘└──┘└────┘  └────
typ  ──────┘└──┘└────┘└┘└────
doc  ──────┘└──┘└────┘  └────
txt  ──────┘└──┘└────┘  └────
par  ──────┘└──┘└────┘  └────
pid  ────────────────┘  └────
st   ────────────────────────
229         <|> apply I4 _ _ _
id                    └┘
src  ──────┘└──┘└────┘  └──────
typ  ──────┘└──┘└────┘└┘└──────
doc  ──────┘└──┘└────┘  └──────
txt  ──────┘└──┘└────┘  └──────
par  ──────┘└──┘└────┘  └──────
pid  ────────────────┘  └──────
st   ──────────────────────────
230         <|> apply I5 _
id                    └┘
src  ──────┘└──┘└────┘  └──
typ  ──────┘└──┘└────┘└┘└──
doc  ──────┘└──┘└────┘  └──
txt  ──────┘└──┘└────┘  └──
par  ──────┘└──┘└────┘  └──
pid  ────────────────┘  └──
st   ──────────────────────
231         <|> apply I6 _ _
id                    └┘
src  ──────┘└──┘└────┘  └────
typ  ──────┘└──┘└────┘└┘└────
doc  ──────┘└──┘└────┘  └────
txt  ──────┘└──┘└────┘  └────
par  ──────┘└──┘└────┘  └────
pid  ────────────────┘  └────
st   ────────────────────────
232         <|> assume x },
src  ──────┘└──┘└───────┘
typ  ──────┘└──┘└───────┘
doc  ──────┘└──┘└───────┘
txt  ──────┘└──┘└───────┘
par  ──────┘└──┘└───────┘
pid  ───────────────────┘
st   ───────────────────┘
233  end
st   └─┘
234  
235  /-- Compactness of candidates (in bounded_continuous_functions) follows -/
236  private lemma compact_candidates_b : compact (candidates_b α β) :=
id                                                               
typ                                                              
237  begin
238    refine arzela_ascoli₂ (Icc 0 (max_var α β)) compact_Icc (candidates_b α β) closed_candidates_b _ _,
239    { rintros f ⟨x1, x2⟩ hf,
240      simp only [set.mem_Icc],
241      exact ⟨candidates_nonneg hf, candidates_le_max_var hf⟩ },
st                                                              └┘
242    { refine equicontinuous_of_continuity_modulus (λt, 2 * max_var α β * t) _ _ _,
id                                                                    
typ                                                                   
243      { have : tendsto (λ (t : ℝ), 2 * (max_var α β : ℝ) * t) (𝓝 0) (𝓝 (2 * max_var α β * 0)) :=
id                                                                                      
typ                                                                                     
244          tendsto_const_nhds.mul tendsto_id,
245        simpa using this },
st                          └┘
246      { assume x y f hf,
247        exact candidates_lipschitz hf _ _ } }
st                                           └───
248  end
st   ──┘
249  
250  /-- We will then choose the candidate minimizing the Hausdorff distance. Except that we are not
251  in a metric space setting, so we need to define our custom version of Hausdorff distance,
252  called HD, and prove its basic properties. -/
253  def HD (f : Cb α β) := max (supr (λx:α, infi (λy:β, f (inl x, inr y))))
id                                                                
typ                                                               
254                             (supr (λy:β, infi (λx:α, f (inl x, inr y))))
id                                                                    
typ                                                                   
255  
256  /- We will show that HD is continuous on bounded_continuous_functions, to deduce that its
257  minimum on the compact set candidates_b is attained. Since it is defined in terms of
258  infimum and supremum on ℝ, which is only conditionnally complete, we will need all the time
259  to check that the defining sets are bounded below or above. This is done in the next few
260  technical lemmas -/
261  
262  lemma HD_below_aux1 {f : Cb α β} (C : ℝ) {x : α} : bdd_below (range (λ (y : β), f (inl x, inr y) + C)) :=
id                                                                                               
src                                        
typ                                                                                              
263  let ⟨cf, hcf⟩ := (real.bounded_iff_bdd_below_bdd_above.1 bounded_range).1 in
id        └┘
typ       └┘
264  ⟨cf + C, forall_range_iff.2 (λi, add_le_add_right ((λx, hcf (mem_range_self x)) _) _)⟩
id                                
typ                               
265  
266  private lemma HD_bound_aux1 (f : Cb α β) (C : ℝ) : bdd_above (range (λ (x : α), infi (λy:β, f (inl x, inr y) + C))) :=
id                                                                                                           
src                                                
typ                                                                                                          
267  begin
268    rcases (real.bounded_iff_bdd_below_bdd_above.1 bounded_range).2 with ⟨Cf, hCf⟩,
269    refine ⟨Cf + C, forall_range_iff.2 (λx, _)⟩,
id             └┘                          
typ            └┘                          
270    calc infi (λy:β, f (inl x, inr y) + C) ≤ f (inl x, inr (default β)) + C :
id                                                                    
typ                                                                   
271      cinfi_le (HD_below_aux1 C)
id                               
typ                              
272      ... ≤ Cf + C : add_le_add ((λx, hCf (mem_range_self x)) _) (le_refl _)
id             └┘
typ            └┘
273  end
st   └─┘
274  
275  lemma HD_below_aux2 {f : Cb α β} (C : ℝ) {y : β} : bdd_below (range (λ (x : α), f (inl x, inr y) + C)) :=
id                                                                                               
src                                        
typ                                                                                              
276  let ⟨cf, hcf⟩ := (real.bounded_iff_bdd_below_bdd_above.1 bounded_range).1 in
id        └┘
typ       └┘
277  ⟨cf + C, forall_range_iff.2 (λi, add_le_add_right ((λx, hcf (mem_range_self x)) _) _)⟩
id                                
typ                               
278  
279  private lemma HD_bound_aux2 (f : Cb α β) (C : ℝ) : bdd_above (range (λ (y : β), infi (λx:α, f (inl x, inr y) + C))) :=
id                                                                                                           
src                                                
typ                                                                                                          
280  begin
281    rcases (real.bounded_iff_bdd_below_bdd_above.1 bounded_range).2 with ⟨Cf, hCf⟩,
282    refine ⟨Cf + C, forall_range_iff.2 (λy, _)⟩,
id             └┘                          
typ            └┘                          
283    calc infi (λx:α, f (inl x, inr y) + C) ≤ f (inl (default α), inr y) + C :
id                                                                     
typ                                                                    
284      cinfi_le (HD_below_aux2 C)
id                               
typ                              
285    ... ≤ Cf + C : add_le_add ((λx, hCf (mem_range_self x)) _) (le_refl _)
id           └┘
typ          └┘
286  end
st   └─┘
287  
288  /-- Explicit bound on HD (dist). This means that when looking for minimizers it will
289  be sufficient to look for functions with HD(f) bounded by this bound. -/
290  lemma HD_candidates_b_dist_le : HD (candidates_b_dist α β) ≤ diam (univ : set α) + 1 + diam (univ : set β) :=
id                                                                           └┘                       └┘  
src                                                                            └┘                        └┘
typ                                                                          └┘                       └┘  
291  begin
292    refine max_le (csupr_le (λx, _)) (csupr_le (λy, _)),
293    { have A : infi (λy:β, candidates_b_dist α β (inl x, inr y)) ≤ candidates_b_dist α β (inl x, inr (default β)) :=
id                                                                                                             
typ                                                                                                            
294        cinfi_le (by simpa using HD_below_aux1 0),
295      have B : dist (inl x) (inr (default β)) ≤ diam (univ : set α) + 1 + diam (univ : set β) := calc
id                                                                                      └─┘ 
src                                                                                       └─┘
typ                                                                                     └─┘ 
296        dist (inl x) (inr (default β)) = dist x (default α) + 1 + dist (default β) (default β) : rfl
id                                               
typ                                              
297        ... ≤ diam (univ : set α) + 1 + diam (univ : set β) :
id                                                     └─┘ 
src                                                     └─┘
typ                                                    └─┘ 
298        begin
299          apply add_le_add (add_le_add _ (le_refl _)),
300          exact dist_le_diam_of_mem (bounded_of_compact (compact_univ)) (mem_univ _) (mem_univ _),
301          exact dist_le_diam_of_mem (bounded_of_compact (compact_univ)) (mem_univ _) (mem_univ _)
302        end,
st         └─┘
303      exact le_trans A B },
st                          └┘
304    { have A : infi (λx:α, candidates_b_dist α β (inl x, inr y)) ≤ candidates_b_dist α β (inl (default α), inr y) :=
id                                                                                                              
typ                                                                                                             
305        cinfi_le (by simpa using HD_below_aux2 0),
306      have B : dist (inl (default α)) (inr y) ≤ diam (univ : set α) + 1 + diam (univ : set β) := calc
id                                                                                      └─┘ 
src                                                                                       └─┘
typ                                                                                     └─┘ 
307        dist (inl (default α)) (inr y) = dist (default α) (default α) + 1 + dist (default β) y : rfl
id                                                                                              
typ                                                                                             
308        ... ≤ diam (univ : set α) + 1 + diam (univ : set β) :
id                                                     └─┘ 
src                                                     └─┘
typ                                                    └─┘ 
309        begin
310          apply add_le_add (add_le_add _ (le_refl _)),
311          exact dist_le_diam_of_mem (bounded_of_compact (compact_univ)) (mem_univ _) (mem_univ _),
312          exact dist_le_diam_of_mem (bounded_of_compact (compact_univ)) (mem_univ _) (mem_univ _)
313        end,
st         └─┘
314      exact le_trans A B },
st                          └┘
315  end
st   └─┘
316  
317  /- To check that HD is continuous, we check that it is Lipschitz. As HD is a max, we
318  prove separately inequalities controlling the two terms (relying too heavily on copy-paste...) -/
319  private lemma HD_lipschitz_aux1 (f g : Cb α β) :
id                                              
typ                                             
320    supr (λx:α, infi (λy:β, f (inl x, inr y))) ≤ supr (λx:α, infi (λy:β, g (inl x, inr y))) + dist f g :=
id                                                                                  
typ                                                                                 
321  begin
322    rcases (real.bounded_iff_bdd_below_bdd_above.1 bounded_range).1 with ⟨cg, hcg⟩,
323    have Hcg : ∀x, cg ≤ g x := λx, hcg (mem_range_self x),
id                    └┘
typ                   └┘
324    rcases (real.bounded_iff_bdd_below_bdd_above.1 bounded_range).1 with ⟨cf, hcf⟩,
325    have Hcf : ∀x, cf ≤ f x := λx, hcf (mem_range_self x),
id                    └┘
typ                   └┘
326  
327    -- prove the inequality but with `dist f g` inside, by using inequalities comparing
328    -- supr to supr and infi to infi
329    have Z : supr (λx:α, infi (λy:β, f (inl x, inr y))) ≤ supr (λx:α, infi (λy:β, g (inl x, inr y) + dist f g)) :=
id                                                                               
typ                                                                              
330      csupr_le_csupr (HD_bound_aux1 _ (dist f g))
331        (λx, cinfi_le_cinfi ⟨cf, forall_range_iff.2(λi, Hcf _)⟩ (λy, coe_le_coe_add_dist)),
id                             └┘                                  
typ                            └┘                                  
332    -- move the `dist f g` out of the infimum and the supremum, arguing that continuous monotone maps
333    -- (here the addition of `dist f g`) preserve infimum and supremum
334    have E1 : ∀x, infi (λy:β, g (inl x, inr y)) + dist f g =
id                
typ               
335               infi ((λz, z + dist f g) ∘ (λy:β, (g (inl x, inr y)))),
id                                              
typ                                             
336    { assume x,
337      refine cinfi_of_cinfi_of_monotone_of_continuous (_ : continuous (λ (z : ℝ), z + dist f g)) _ _,
338      { exact continuous_id.add continuous_const },
st                                                  └┘
339      { assume x y hx, simpa },
st                              └┘
340      { show bdd_below (range (λ (y : β), g (inl x, inr y))),
id                                                 
typ                                                
341          from ⟨cg, forall_range_iff.2(λi, Hcg _)⟩ } },
id                 └┘                      
typ                └┘                      
st                                                    └──┘
342    have E2 : supr (λx:α, infi (λy:β, g (inl x, inr y))) + dist f g =
343           supr ((λz, z + dist f g) ∘ (λx:α, infi (λy:β, g (inl x, inr y)))),
id                                                     
typ                                                    
344    { refine csupr_of_csupr_of_monotone_of_continuous (_ : continuous (λ (z : ℝ), z + dist f g)) _ _,
345      { exact continuous_id.add continuous_const },
st                                                  └┘
346      { assume x y hx, simpa },
st                              └┘
347      { by simpa using HD_bound_aux1 _ 0 } },
st                                          └──┘
348    -- deduce the result from the above two steps
349    simp only [add_comm] at Z,
350    simpa [E2, E1, function.comp]
351  end
st   └─┘
352  
353  private lemma HD_lipschitz_aux2 (f g : Cb α β) :
id                                              
typ                                             
354    supr (λy:β, infi (λx:α, f (inl x, inr y))) ≤ supr (λy:β, infi (λx:α, g (inl x, inr y))) + dist f g :=
id                                                                                 
typ                                                                                
355  begin
356    rcases (real.bounded_iff_bdd_below_bdd_above.1 bounded_range).1 with ⟨cg, hcg⟩,
357    have Hcg : ∀x, cg ≤ g x := λx, hcg (mem_range_self x),
id                    └┘
typ                   └┘
358    rcases (real.bounded_iff_bdd_below_bdd_above.1 bounded_range).1 with ⟨cf, hcf⟩,
359    have Hcf : ∀x, cf ≤ f x := λx, hcf (mem_range_self x),
id                    └┘
typ                   └┘
360  
361    -- prove the inequality but with `dist f g` inside, by using inequalities comparing
362    -- supr to supr and infi to infi
363    have Z : supr (λy:β, infi (λx:α, f (inl x, inr y))) ≤ supr (λy:β, infi (λx:α, g (inl x, inr y) + dist f g)) :=
id                                                                               
typ                                                                              
364      csupr_le_csupr (HD_bound_aux2 _ (dist f g))
365        (λy, cinfi_le_cinfi  ⟨cf, forall_range_iff.2(λi, Hcf _)⟩ (λy, coe_le_coe_add_dist)),
id                              └┘                                  
typ                             └┘                                  
366    -- move the `dist f g` out of the infimum and the supremum, arguing that continuous monotone maps
367    -- (here the addition of `dist f g`) preserve infimum and supremum
368    have E1 : ∀y, infi (λx:α, g (inl x, inr y)) + dist f g =
id                
typ               
369               infi ((λz, z + dist f g) ∘ (λx:α, (g (inl x, inr y)))),
id                                              
typ                                             
370    { assume y,
371      refine cinfi_of_cinfi_of_monotone_of_continuous (_ : continuous (λ (z : ℝ), z + dist f g)) _ _,
372      { exact continuous_id.add continuous_const },
st                                                  └┘
373      { assume x y hx, simpa },
st                              └┘
374      { show bdd_below (range (λx:α, g (inl x, inr y))),
id                                                   
typ                                                  
375          from ⟨cg, forall_range_iff.2(λi, Hcg _)⟩ } },
id                 └┘                      
typ                └┘                      
st                                                    └──┘
376    have E2 : supr (λy:β, infi (λx:α, g (inl x, inr y))) + dist f g =
377           supr ((λz, z + dist f g) ∘ (λy:β, infi (λx:α, g (inl x, inr y)))),
id                                                     
typ                                                    
378    { refine csupr_of_csupr_of_monotone_of_continuous (_ : continuous (λ (z : ℝ), z + dist f g)) _ _,
379      { exact continuous_id.add continuous_const },
st                                                  └┘
380      { assume x y hx, simpa },
st                              └┘
381      { by simpa using HD_bound_aux2 _ 0 } },
st                                          └──┘
382    -- deduce the result from the above two steps
383    simp only [add_comm] at Z,
384    simpa [E2, E1, function.comp]
385  end
st   └─┘
386  
387  private lemma HD_lipschitz_aux3 (f g : Cb α β) : HD f ≤ HD g + dist f g :=
id                                              
typ                                             
388  max_le (le_trans (HD_lipschitz_aux1 f g) (add_le_add_right (le_max_left _ _) _))
389         (le_trans (HD_lipschitz_aux2 f g) (add_le_add_right (le_max_right _ _) _))
390  
391  /-- Conclude that HD, being Lipschitz, is continuous -/
392  private lemma HD_continuous : continuous (HD : Cb α β → ℝ) :=
id                                                         
src                                                          
typ                                                        
393  lipschitz_with.to_continuous (lipschitz_with.one_of_le_add HD_lipschitz_aux3)
394  
395  end constructions --section
396  
397  section consequences
398  variables (α : Type u) (β : Type v) [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β]
id                  └┘          └──┘    └──────────┘     └───────────┘     └──────┘     └──────────┘     └───────────┘     └──────┘
src                                       └──────────┘     └───────────┘     └──────┘     └──────────┘     └───────────┘     └──────┘
typ                 └┘          └──┘    └──────────┘     └───────────┘     └──────┘     └──────────┘     └───────────┘     └──────┘
doc                                       └──────────┘     └───────────┘                  └──────────┘     └───────────┘
399  
400  /- Now that we have proved that the set of candidates is compact, and that HD is continuous,
401  we can finally select a candidate minimizing HD. This will be the candidate realizing the
402  optimal coupling. -/
403  private lemma exists_minimizer : ∃f ∈ candidates_b α β, ∀g ∈ candidates_b α β, HD f ≤ HD g :=
id                                       └──────────┘       └──────────┘    └┘   └┘ 
src                                       └──────────┘         └──────────┘      └┘    └┘
typ                                      └──────────┘       └──────────┘    └┘   └┘ 
doc                                        └──────────┘           └──────────┘      └┘     └┘
404  compact_candidates_b.exists_forall_le candidates_b_nonempty HD_continuous.continuous_on
id   └──────────────────┘└───────────────┘ └───────────────────┘ └───────────┘└────────────┘
src  └──────────────────┘└───────────────┘ └───────────────────┘ └───────────┘└────────────┘
typ  └──────────────────┘└───────────────┘ └───────────────────┘ └───────────┘└────────────┘
doc  └──────────────────┘└───────────────┘                       └───────────┘
405  
406  private definition optimal_GH_dist : Cb α β := classical.some (exists_minimizer α β)
id                                        └┘      └────────────┘  └──────────────┘  
src                                       └┘        └────────────┘  └──────────────┘
typ                                       └┘      └────────────┘  └──────────────┘  
407  
408  private lemma optimal_GH_dist_mem_candidates_b : optimal_GH_dist α β ∈ candidates_b α β :=
id                                                    └─────────────┘    └──────────┘  
src                                                   └─────────────┘      └──────────┘
typ                                                   └─────────────┘    └──────────┘  
doc                                                                         └──────────┘
409  by cases (classical.some_spec (exists_minimizer α β)); assumption
id             └─────────────────┘  └──────────────┘  
src     └────┘ └─────────────────┘ └──────────────┘  └┘  └──────────
typ     └────┘ └─────────────────┘ └──────────────┘└┘  └──────────
doc     └────┘                                       └┘  └──────────
txt     └────┘                                       └┘  └──────────
par     └────┘                                       └┘  └──────────
pid                                                 └┘            
st     └───────────────────────────────────────────────────────────────
410  
src  
typ  
doc  
txt  
par  
pid  
st   
411  private lemma HD_optimal_GH_dist_le (g : Cb α β) (hg : g ∈ candidates_b α β) : HD (optimal_GH_dist α β) ≤ HD g :=
id                                            └┘            └──────────┘      └┘  └─────────────┘     └┘ 
src                                           └┘               └──────────┘        └┘  └─────────────┘       └┘
typ                                           └┘            └──────────┘      └┘  └─────────────┘     └┘ 
doc                                                             └──────────┘        └┘                         └┘
412  let ⟨Z1, Z2⟩ := classical.some_spec (exists_minimizer α β) in Z2 g hg
id   └─┘      └┘     └─────────────────┘  └──────────────┘           └┘
src                  └─────────────────┘  └──────────────┘
typ  └─┘      └┘     └─────────────────┘  └──────────────┘           └┘
413  
414  /-- With the optimal candidate, construct a premetric space structure on α ⊕ β, on which the
415  predistance is given by the candidate. Then, we will identify points at 0 predistance
416  to obtain a genuine metric space -/
417  def premetric_optimal_GH_dist : premetric_space (α ⊕ β) :=
id                                   └─────────────┘    
src                                  └─────────────┘    
typ                                  └─────────────┘    
418  { dist := λp q, optimal_GH_dist α β (p, q),
id                 └─────────────┘     
src                  └─────────────┘     
typ                └─────────────┘     
419    dist_self := λx, candidates_refl (optimal_GH_dist_mem_candidates_b α β),
id                     └─────────────┘  └──────────────────────────────┘  
src                     └─────────────┘  └──────────────────────────────┘
typ                    └─────────────┘  └──────────────────────────────┘  
420    dist_comm := λx y, candidates_symm (optimal_GH_dist_mem_candidates_b α β),
id                      └─────────────┘  └──────────────────────────────┘  
src                       └─────────────┘  └──────────────────────────────┘
typ                     └─────────────┘  └──────────────────────────────┘  
421    dist_triangle := λx y z, candidates_triangle (optimal_GH_dist_mem_candidates_b α β) }
id                           └─────────────────┘  └──────────────────────────────┘  
src                             └─────────────────┘  └──────────────────────────────┘
typ                          └─────────────────┘  └──────────────────────────────┘  
422  
423  local attribute [instance] premetric_optimal_GH_dist premetric.dist_setoid
id                              └───────────────────────┘ └───────────────────┘
src                             └───────────────────────┘ └───────────────────┘
typ                             └───────────────────────┘ └───────────────────┘
doc                             └───────────────────────┘ └───────────────────┘
424  
425  /-- A metric space which realizes the optimal coupling between α and β -/
426  @[derive [metric_space]] definition optimal_GH_coupling : Type* :=
id             └──────────┘
src            └──────────┘
typ            └──────────┘
doc    └────┘  └──────────┘
427  premetric.metric_quot (α ⊕ β)
id   └───────────────────┘    
src  └───────────────────┘    
typ  └───────────────────┘    
doc  └───────────────────┘
428  
429  /-- Injection of α in the optimal coupling between α and β -/
430  def optimal_GH_injl (x : α) : optimal_GH_coupling α β := ⟦inl x⟧
id                                └─────────────────┘      └─┘ 
src                                └─────────────────┘        └─┘  
typ                               └─────────────────┘      └─┘ 
doc                                └─────────────────┘
431  
432  /-- The injection of α in the optimal coupling between α and β is an isometry. -/
433  lemma isometry_optimal_GH_injl : isometry (optimal_GH_injl α β) :=
id                                    └──────┘  └─────────────┘  
src                                   └──────┘  └─────────────┘
typ                                   └──────┘  └─────────────┘  
doc                                   └──────┘  └─────────────┘
434  begin
st   └─────
435    refine isometry_emetric_iff_metric.2 (λx y, _),
id            └─────────────────────────┘
src    └─────┘└─────────────────────────┘└─┘  └─────┘
typ    └─────┘└─────────────────────────┘└─┘  └─────┘
doc    └─────┘└─────────────────────────┘└─┘  └─────┘
txt    └─────┘                           └─┘  └─────┘
par    └─────┘                           └─┘  └─────┘
pid                                     └─┘  └─────┘
st   ───────────────────────────────────────────────┘└─
436    change dist ⟦inl x⟧ ⟦inl y⟧ = dist x y,
id                        └─┘     └──┘  
src    └─────┘         └─┘  └──┘ 
typ    └─────┘         └─┘  └──┘
doc    └─────┘                      
txt    └─────┘                      
par    └─────┘                      
pid                                
st   ───────────────────────────────────────┘└─
437    exact candidates_dist_inl (optimal_GH_dist_mem_candidates_b α β) _ _,
id           └─────────────────┘  └──────────────────────────────┘  
src    └────┘└─────────────────┘ └──────────────────────────────┘  └───┘
typ    └────┘└─────────────────┘ └──────────────────────────────┘└───┘
doc    └────┘                                                      └───┘
txt    └────┘                                                      └───┘
par    └────┘                                                      └───┘
pid                                                               └───┘
st   ─────────────────────────────────────────────────────────────────────┘└─
438  end
st   ──┘
439  
440  /-- Injection of β  in the optimal coupling between α and β -/
441  def optimal_GH_injr (y : β) : optimal_GH_coupling α β := ⟦inr y⟧
id                                └─────────────────┘      └─┘ 
src                                └─────────────────┘        └─┘  
typ                               └─────────────────┘      └─┘ 
doc                                └─────────────────┘
442  
443  /-- The injection of β in the optimal coupling between α and β is an isometry. -/
444  lemma isometry_optimal_GH_injr : isometry (optimal_GH_injr α β) :=
id                                    └──────┘  └─────────────┘  
src                                   └──────┘  └─────────────┘
typ                                   └──────┘  └─────────────┘  
doc                                   └──────┘  └─────────────┘
445  begin
st   └─────
446    refine isometry_emetric_iff_metric.2 (λx y, _),
id            └─────────────────────────┘
src    └─────┘└─────────────────────────┘└─┘  └─────┘
typ    └─────┘└─────────────────────────┘└─┘  └─────┘
doc    └─────┘└─────────────────────────┘└─┘  └─────┘
txt    └─────┘                           └─┘  └─────┘
par    └─────┘                           └─┘  └─────┘
pid                                     └─┘  └─────┘
st   ───────────────────────────────────────────────┘└─
447    change dist ⟦inr x⟧ ⟦inr y⟧ = dist x y,
id                        └─┘     └──┘  
src    └─────┘         └─┘  └──┘ 
typ    └─────┘         └─┘  └──┘
doc    └─────┘                      
txt    └─────┘                      
par    └─────┘                      
pid                                
st   ───────────────────────────────────────┘└─
448    exact candidates_dist_inr (optimal_GH_dist_mem_candidates_b α β) _ _,
id           └─────────────────┘  └──────────────────────────────┘  
src    └────┘└─────────────────┘ └──────────────────────────────┘  └───┘
typ    └────┘└─────────────────┘ └──────────────────────────────┘└───┘
doc    └────┘                                                      └───┘
txt    └────┘                                                      └───┘
par    └────┘                                                      └───┘
pid                                                               └───┘
st   ─────────────────────────────────────────────────────────────────────┘└─
449  end
st   ──┘
450  
451  /-- The optimal coupling between two compact spaces α and β is still a compact space -/
452  instance compact_space_optimal_GH_coupling : compact_space (optimal_GH_coupling α β) :=
id                                                └───────────┘  └─────────────────┘  
src                                               └───────────┘  └─────────────────┘
typ                                               └───────────┘  └─────────────────┘  
doc                                               └───────────┘  └─────────────────┘
453  ⟨begin
st    └─────
454    have : (univ : set (optimal_GH_coupling α β)) =
id                    └─┘  └─────────────────┘       
src    └─────┘     └─┘└─┘ └─────────────────┘  └─┘
typ    └─────┘     └─┘└─┘ └─────────────────┘  └─┘
doc    └─────┘     └─┘    └─────────────────┘  └─┘ 
txt    └─────┘     └─┘                         └─┘ 
par    └─────┘     └─┘                         └─┘ 
pid    └───┘└┘     └─┘                         └─┘ 
st   ──────────────────────────────────────────────────
455             (optimal_GH_injl α β '' univ) ∪ (optimal_GH_injr α β '' univ),
id               └─────────────┘     └┘         └─────────────┘      └──┘
src  ──────────┘ └─────────────┘  └┘    └┘ └─────────────┘    └──┘
typ  ──────────┘ └─────────────┘  └┘    └┘ └─────────────┘  └──┘
doc  ──────────┘ └─────────────┘        └┘  └─────────────┘        
txt  ──────────┘                        └┘                         
par  ──────────┘                        └┘                         
pid  ──────────┘                        └┘                         
st   ───────────────────────────────────────────────────────────────────────┘└─
456    { refine subset.antisymm (λxc hxc, _) (subset_univ _),
id              └─────────────┘               └─────────┘
src      └─────┘└─────────────┘  └─────────┘ └─────────┘└─┘
typ      └─────┘└─────────────┘  └─────────┘ └─────────┘└─┘
doc      └─────┘                 └─────────┘            └─┘
txt      └─────┘                 └─────────┘            └─┘
par      └─────┘                 └─────────┘            └─┘
pid                             └─────────┘            └─┘
st   ───┘└─────────────────────────────────────────────────┘└─
457      rcases quotient.exists_rep xc with ⟨x, hx⟩,
id              └─────────────────┘ └┘
src      └─────┘└─────────────────┘  └───────────┘
typ      └─────┘└─────────────────┘└┘└───────────┘
doc      └─────┘                     └───────────┘
txt      └─────┘                     └───────────┘
par      └─────┘                     └───────────┘
pid                                 └───────────┘
st   ─────────────────────────────────────────────┘└─
458      cases x; rw ← hx,
id                    └┘
src      └────┘   └───┘
typ      └────┘  └───┘└┘
doc      └────┘   └───┘
txt      └────┘   └───┘
par      └────┘   └───┘
pid                └─┘
st   ───────────────────┘ 
459      { have : ⟦inl x⟧ = optimal_GH_injl α β x := rfl,
id                └─┘     └─────────────┘       └─┘
src            └─┘    └─────────────┘        └─┘
typ            └─┘    └─────────────┘     └─┘
doc                     └─────────────┘        
txt                                            
par                                            
pid                                            
st   ─────┘    └─────┘  └─────────────┘     └──┘└─
460        rw this,
id             └─┘
src         
typ          └─┘
doc         
txt         
par         
pid          
st   ──────┘  └─┘ 
461        exact mem_union_left _ (mem_image_of_mem _ (mem_univ _)) },
id            └────────────┘    └──────────────┘    └──────┘
src        └────┘└────────────┘└┘  └──────────────┘   └──────┘└───┘
typ        └────┘└────────────┘└┘  └──────────────┘   └──────┘└───┘
doc        └────┘              └┘                             └───┘
txt                         └┘                             └───┘
par                         └┘                             └───┘
pid                           └┘                             └──┘
st      └─────┘ └─┘ └─┘   └─┘   └─────┘ └───┘   └──────────┘ 
462      { have : ⟦inr x⟧ = optimal_GH_injr α β x := rfl,
id                 └─┘      └─────────────┘       └─┘
src             └─┘     └─────────────┘        └─┘
typ             └─┘     └─────────────┘     └─┘
doc                     └─────────────┘        
txt                                            
par                                            
pid                                            
st   ─────┘    └─────┘  └─────────────┘     └──┘└─
463        rw this,
id             └─┘
src         
typ          └─┘
doc         
txt         
par         
pid          
st   ──────┘  └─┘ 
464        exact mem_union_right _ (mem_image_of_mem _ (mem_univ _)) } },
id            └─────────────┘    └──────────────┘    └──────┘
src        └────┘└─────────────┘└─┘ └──────────────┘└─┘ └──────┘  
typ        └────┘└─────────────┘└─┘ └──────────────┘└─┘ └──────┘  
doc        └────┘               └─┘                 └─┘           
txt                          └─┘                 └─┘           
par                          └─┘                 └─┘           
pid                            └─┘                 └─┘           
st      └─────┘ └─────┘ └─┘ └─────┘   └─────────────┘      └──┘
465    rw this,
id       └──┘
src     
typ      └──┘
doc     
st      └──┘ 
466    exact (compact_univ.image (isometry_optimal_GH_injl α β).continuous).union
id                             └──────────────────────┘              
src    └────┘                    └──────────────────────┘   
typ    └────┘                    └──────────────────────┘   
doc    └────┘                    └──────────────────────┘      
txt                                                              
par                                                              
pid                                                                
st    └─────┘                                  
467      (compact_univ.image (isometry_optimal_GH_injr α β).continuous)
id        └────────────────┘  └──────────────────────┘        
src     └────────────────┘  └──────────────────────┘      
typ     └────────────────┘  └──────────────────────┘    
doc                         └──────────────────────┘      
txt                                                            
par                                                            
pid                                                            
st                                    
468  end⟩
st   └─┘
469  
470  /-- For any candidate f, HD(f) is larger than or equal to the Hausdorff distance in the
471  optimal coupling. This follows from the fact that HD of the optimal candidate is exactly
472  the Hausdorff distance in the optimal coupling, although we only prove here the inequality
473  we need. -/
474  lemma Hausdorff_dist_optimal_le_HD {f} (h : f ∈ candidates_b α β) :
id                                                 └──────────┘  
src                                                 └──────────┘
typ                                                └──────────┘  
doc                                                  └──────────┘
475    Hausdorff_dist (range (optimal_GH_injl α β)) (range (optimal_GH_injr α β)) ≤ HD f :=
id     └────────────┘  └───┘  └─────────────┘      └───┘  └─────────────┘      └┘ 
src    └────────────┘  └───┘  └─────────────┘        └───┘  └─────────────┘        └┘
typ    └────────────┘  └───┘  └─────────────┘      └───┘  └─────────────┘      └┘ 
doc    └────────────┘  └───┘  └─────────────┘        └───┘  └─────────────┘         └┘
476  begin
st   └───┘
477    refine le_trans (le_of_forall_le_of_dense (λr hr, _)) (HD_optimal_GH_dist_le α β f h),
id            └──────┘  └──────────────────────┘              └───────────────────┘    
src    └─────┘└──────┘ └──────────────────────┘  └────────┘ └───────────────────┘    
typ    └─────┘└──────┘ └──────────────────────┘  └────────┘ └───────────────────┘
doc    └─────┘                                   └────────┘                          
txt    └─────┘                                   └────────┘                          
par    └─────┘                                   └────────┘                          
pid                                             └────────┘                          
st   └─────────────────────────────────────────────────────────────────────────────────────┘
478    have A : ∀ x ∈ range (optimal_GH_injl α β), ∃ y ∈ range (optimal_GH_injr α β), dist x y ≤ r,
id                                                                                             
typ                                                                                            
479    { assume x hx,
480      rcases mem_range.1 hx with ⟨z, hz⟩,
481      rw ← hz,
482      have I1 : supr (λx:α, infi (λy:β, optimal_GH_dist α β (inl x, inr y))) < r :=
id                                                                              
typ                                                                             
483        lt_of_le_of_lt (le_max_left _ _) hr,
484      have I2 : infi (λy:β, optimal_GH_dist α β (inl z, inr y)) ≤
id                                                      
typ                                                     
485          supr (λx:α, infi (λy:β, optimal_GH_dist α β (inl x, inr y))) :=
id                                                    
typ                                                   
486        le_cSup (by simpa using HD_bound_aux1 _ 0) (mem_range_self _),
487      have I : infi (λy:β, optimal_GH_dist α β (inl z, inr y)) < r := lt_of_le_of_lt I2 I1,
id                                                               
typ                                                              
488      rcases exists_lt_of_cInf_lt (range_nonempty _) I with ⟨r', r'range, hr'⟩,
489      rcases mem_range.1 r'range with ⟨z', hz'⟩,
490      existsi [optimal_GH_injr α β z', mem_range_self _],
id                                  └┘
typ                                 └┘
491      have : (optimal_GH_dist α β) (inl z, inr z') ≤ r := begin rw hz', exact le_of_lt hr' end,
id                                             └┘    
typ                                            └┘    
st                                                                                            └─┘
492      exact this },
st                  └┘
493    refine Hausdorff_dist_le_of_mem_dist _ A _,
494    { rcases exists_mem_of_nonempty α with ⟨xα, _⟩,
id                                     
typ                                    
495      have : optimal_GH_injl α β xα ∈ range (optimal_GH_injl α β) := mem_range_self _,
id                                  └┘                           
typ                                 └┘                           
496      rcases A _ this with ⟨y, yrange, hy⟩,
497      exact le_trans dist_nonneg hy },
st                                     └┘
498    { assume y hy,
499      rcases mem_range.1 hy with ⟨z, hz⟩,
500      rw ← hz,
501      have I1 : supr (λy:β, infi (λx:α, optimal_GH_dist α β (inl x, inr y))) < r :=
id                                                                              
typ                                                                             
502        lt_of_le_of_lt (le_max_right _ _) hr,
503      have I2 : infi (λx:α, optimal_GH_dist α β (inl x, inr z)) ≤
id                                                             
typ                                                            
504          supr (λy:β, infi (λx:α, optimal_GH_dist α β (inl x, inr y))) :=
id                                                    
typ                                                   
505        le_cSup (by simpa using HD_bound_aux2 _ 0) (mem_range_self _),
506      have I : infi (λx:α, optimal_GH_dist α β (inl x, inr z)) < r := lt_of_le_of_lt I2 I1,
id                                                               
typ                                                              
507      rcases exists_lt_of_cInf_lt (range_nonempty _) I with ⟨r', r'range, hr'⟩,
508      rcases mem_range.1 r'range with ⟨z', hz'⟩,
509      existsi [optimal_GH_injl α β z', mem_range_self _],
id                                  └┘
typ                                 └┘
510      have : (optimal_GH_dist α β) (inl z', inr z) ≤ r := begin rw hz', exact le_of_lt hr' end,
id                                       └┘          
typ                                      └┘          
st                                                                                            └─┘
511      rw dist_comm,
512      exact this }
st                  └─
513  end
st   ──┘
514  
515  end consequences
516  /- We are done with the construction of the optimal coupling -/
517  end Gromov_Hausdorff_realized
518  
519  end Gromov_Hausdorff